We shall seek to strike a balance between depth and breadth, covering both the foundations and some of the more successful formalisms, techniques, and tools. Below is a tentative list of topics and their schedule:
• Introduction (.5 week: 9/19a)
• Formal Logic: Propositional and First-Order Logics (1.5 weeks: 9/19b, 9/26)
• Verification of Sequential Programs: Hoare Logic (1 week: 10/3)
• Predicate Transformers and Program Derivation (1 week: 10/17)
• Tool Support: Why, Spec# (1 week: 10/24)
• Procedures + Object Orientation (1 week: 10/31)
• Data Refinement + Formal Methods: Z, VDM, and B (3 weeks: 11/7, 11/14, 11/21)
• Concurrent, Reactive Systems: Owicki-Gries Method, UNITY, Linear Temporal Logic (2 weeks: 11/28, 12/5)
• Modular/Compositional Reasoning (1 week: 12/12)
• Simply-Typed Lambda Calculus + the Coq Proof Assistant (1 week: 12/19)
• Polymorphic Types + the Coq Proof Assistant (1 week: 12/26)
• Final (2008/01/02)
• Selected Topics: Proof-Carrying Code (1 week: 2008/01/09)
• Selected Topics: Separation Logic (1 week: 2008/01/16)